wlan.4.jani:model: info: wlan.4 is an MDP model.
wlan.4.jani:variables[7]: info: Expanding variable "s1" into 12 locations in automaton "station1".
wlan.4.jani:variables[12]: info: Expanding variable "s2" into 12 locations in automaton "station2".
wlan.4.jani: info: Need 16 bytes per state.
wlan.4.jani: info: Explored 345000 states for COL=0.
wlan.4.jani:properties[2]: warning: Computing minimum expected reward in property "cost_min" without checking for zero-reward end components.
Peak memory usage: 181 MB
Analysis results for wlan.4.jani
Experiment COL=0
+ State space exploration
State size: 16 bytes
States: 345000
Transitions: 440206
Branches: 762252
Rate: 397924 states/s
Time: 0.9 s
+ Property cost_min
Value: 7625
Bounds: [7625, infinity)
Time: 13.0 s
+ Precomputations
Max. prob. 1 states: 345000
Time for max. prob. 1 states: 12.9 s
+ Essential states
Iterations: 14
Essential states: 6151
Transitions: 10499
Branches: 81553
Time: 0.1 s
+ Value iteration
Final error: 0
Iterations: 8
Time: 0.0 s
Exported results to file "/out.txt".